(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(set-option :model_validate true)
(set-option :model true)
(set-option :smt.arith.solver 6)
(declare-const r1 Real)
(declare-const r3 Real)

(assert v0)
(assert v1)
(assert v3)
(assert (= (* (/ 271866967.0 50000000.0) r1 9.0 r3) 9.0))
(assert v4)
(check-sat-using smt)
(exit)

(set-logic NRA)
(set-option :model_validate true)
(set-option :model true)
(set-option :smt.arith.solver 6)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const v4 Bool)
(assert v0)
(assert (=> v2 (or v2 v0 v1 v3 v2 v0 v0 v1)))
(declare-const v5 Bool)
(declare-const v6 Bool)
(assert v1)
(declare-const v7 Bool)
(declare-const v8 Bool)
(assert (or v2 v0 v1 v3 v2 v0 v0 v1))
(assert v4)
(declare-const v9 Bool)
(assert (= (* r1 r3 r2 5.43733934) r2 9.0))
;(check-sat)
;(exit)
;(apply (then simplify max-bv-sharing))
;(apply (then simplify max-bv-sharing dom-simplify))
(apply (then simplify max-bv-sharing dom-simplify elim-uncnstr ctx-solver-simplify))
;(check-sat-using (then simplify max-bv-sharing dom-simplify elim-uncnstr ctx-solver-simplify smt))
;(check-sat-using (then simplify max-bv-sharing elim-uncnstr ctx-solver-simplify smt))